T:Type, f:(TT), x:T. ((f(x) = x))  f(x) = f+(x) 

latex

Definitions

y = f+(x), P & Q, x:A  B(x), f(a), Void, Type, x:A. B(x), x:AB(x), s = t, P  Q, False, A, y is f*(x), [car / cdr], [], A List, last(L), <a, b>, , , Unit, (xL.P(x)), xL. P(x), |r|, x f y, A c B, a < b, |g|, a <p b, a  b, |p|, a ~ b, b | a, x:A. B(x), x,y:A//B(x;y), b, Atom, Dec(P), P  Q, left + right, s ~ t, , SQType(T), {T}, tl(l), i z j, i <z j, hd(l), l[i], n+m, #$n, a < b, {i..j}, {x:A| B(x)} , , i  j < k, A  B, , type List, y=f*(x) via L, t  T

Lemmas

fun-path wf, guard wf, decidable int equal, le wf, int seg wf, false wf, not wf, fun-connected wf, strict-fun-connected wf